YES(O(1),O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We add following dependency tuples: Strict DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#2^#(nil(), @x) -> c_5() , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , group3#3^#(nil(), @x, @y) -> c_7() , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) , zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#2^#(nil(), @x) -> c_5() , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , group3#3^#(nil(), @x, @y) -> c_7() , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) , zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {3,5,7,10,12,14} by applications of Pre({3,5,7,10,12,14}) = {1,2,4,8,9,11}. Here rules are labeled as follows: DPs: { 1: group3^#(@l) -> c_1(group3#1^#(@l)) , 2: group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , 3: group3#1^#(nil()) -> c_3() , 4: group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , 5: group3#2^#(nil(), @x) -> c_5() , 6: group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , 7: group3#3^#(nil(), @x, @y) -> c_7() , 8: zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , 9: zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , 10: zip3#1^#(nil(), @l2, @l3) -> c_10() , 11: zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , 12: zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , 13: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) , 14: zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Weak DPs: { group3#1^#(nil()) -> c_3() , group3#2^#(nil(), @x) -> c_5() , group3#3^#(nil(), @x, @y) -> c_7() , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { group3#1^#(nil()) -> c_3() , group3#2^#(nil(), @x) -> c_5() , group3#3^#(nil(), @x, @y) -> c_7() , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component: Problem (R): ------------ Strict DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } Weak DPs: { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } StartTerms: basic terms Strategy: innermost Problem (S): ------------ Strict DPs: { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } StartTerms: basic terms Strategy: innermost Overall, the transformation results in the following sub-problem(s): Generated new problems: ----------------------- R) Strict DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } Weak DPs: { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } StartTerms: basic terms Strategy: innermost This problem was proven YES(O(1),O(n^1)). S) Strict DPs: { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } StartTerms: basic terms Strategy: innermost This problem was proven YES(O(1),O(n^1)). Proofs for generated problems: ------------------------------ R) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } Weak DPs: { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: group3^#(@l) -> c_1(group3#1^#(@l)) , 2: group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , 3: group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_6) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [::](x1, x2) = [1] x1 + [1] x2 + [1] [nil] = [0] [tuple#3](x1, x2, x3) = [0] [group3^#](x1) = [1] x1 + [1] [c_1](x1) = [1] x1 + [0] [group3#1^#](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [0] [group3#2^#](x1, x2) = [1] x1 + [0] [c_4](x1) = [1] x1 + [0] [group3#3^#](x1, x2, x3) = [1] x1 + [0] [c_6](x1) = [1] x1 + [0] [zip3^#](x1, x2, x3) = [0] [zip3#1^#](x1, x2, x3) = [0] [zip3#2^#](x1, x2, x3, x4) = [0] [zip3#3^#](x1, x2, x3, x4, x5) = [0] This order satisfies following ordering constraints [group3^#(@l)] = [1] @l + [1] > [1] @l + [0] = [c_1(group3#1^#(@l))] [group3#1^#(::(@x, @xs))] = [1] @x + [1] @xs + [1] > [1] @xs + [0] = [c_2(group3#2^#(@xs, @x))] [group3#2^#(::(@y, @ys), @x)] = [1] @y + [1] @ys + [1] > [1] @ys + [0] = [c_4(group3#3^#(@ys, @x, @y))] [group3#3^#(::(@z, @zs), @x, @y)] = [1] @z + [1] @zs + [1] >= [1] @zs + [1] = [c_6(group3^#(@zs))] Consider the set of all dependency pairs DPs: { 1: group3^#(@l) -> c_1(group3#1^#(@l)) , 2: group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , 3: group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , 4: group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {1,2,3}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Wall-time: 0.155536s CPU-time: 1.514s S) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_11) = {1}, Uargs(c_13) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [::](x1, x2) = [1] x1 + [1] x2 + [1] [nil] = [0] [tuple#3](x1, x2, x3) = [0] [group3^#](x1) = [0] [group3#1^#](x1) = [0] [group3#2^#](x1, x2) = [0] [group3#3^#](x1, x2, x3) = [0] [zip3^#](x1, x2, x3) = [1] x1 + [0] [c_8](x1) = [1] x1 + [0] [zip3#1^#](x1, x2, x3) = [1] x1 + [0] [c_9](x1) = [1] x1 + [0] [zip3#2^#](x1, x2, x3, x4) = [1] x4 + [1] [c_11](x1) = [1] x1 + [0] [zip3#3^#](x1, x2, x3, x4, x5) = [1] x3 + [1] [c_13](x1) = [1] x1 + [0] This order satisfies following ordering constraints [zip3^#(@l1, @l2, @l3)] = [1] @l1 + [0] >= [1] @l1 + [0] = [c_8(zip3#1^#(@l1, @l2, @l3))] [zip3#1^#(::(@x, @xs), @l2, @l3)] = [1] @x + [1] @xs + [1] >= [1] @xs + [1] = [c_9(zip3#2^#(@l2, @l3, @x, @xs))] [zip3#2^#(::(@y, @ys), @l3, @x, @xs)] = [1] @xs + [1] >= [1] @xs + [1] = [c_11(zip3#3^#(@l3, @x, @xs, @y, @ys))] [zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys)] = [1] @xs + [1] > [1] @xs + [0] = [c_13(zip3^#(@xs, @ys, @zs))] Consider the set of all dependency pairs DPs: { 1: zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , 2: zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , 3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , 4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {4}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Wall-time: 0.224067s CPU-time: 1.951s Hurray, we answered YES(O(1),O(n^1))